\begin{tabbing}
basic
\\[0ex]IsBilinear($A$;$B$;$C$;${\it +a}$;${\it +b}$;${\it +c}$;$f$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($\forall$$a_{1}$, $a_{2}$:$A$, $b$:$B$. (($a_{1}$ ${\it +a}$ $a_{2}$) $f$ $b$) = (($a_{1}$ $f$ $b$) ${\it +c}$ ($a_{2}$ $f$ $b$)))\+
\\[0ex]\& ($\forall$$a$:$A$, $b_{1}$, $b_{2}$:$B$. ($a$ $f$ ($b_{1}$ ${\it +b}$ $b_{2}$)) = (($a$ $f$ $b_{1}$) ${\it +c}$ ($a$ $f$ $b_{2}$)))
\-
\end{tabbing}